Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Port VST 2.x to CompCert master #781

Merged
merged 15 commits into from
Jul 28, 2024
Merged

Port VST 2.x to CompCert master #781

merged 15 commits into from
Jul 28, 2024

Conversation

andrew-appel
Copy link
Collaborator

@andrew-appel andrew-appel commented Jul 24, 2024 •
edited
Loading

AbsInt/CompCert@f92facf

which will (with future changes) become CompCert 3.15

@andrew-appel andrew-appel changed the title Port VST 2.x to CompCert master https://github.com/AbsInt/CompCert/co… Port VST 2.x to CompCert master Jul 24, 2024
@andrew-appel andrew-appel mentioned this pull request Jul 24, 2024
Closed
@andrew-appel andrew-appel requested a review from mansky1 July 24, 2024 18:34
@andrew-appel
Copy link
Collaborator Author

Note to @mansky1
These changes are worth porting to the vst_on_iris branch.
Also: certain .c files in atomics/ or in concurrency/ don't successfully build on MacOS, I think because <threads.h> is not compatible. So one could run clightgen on those files on Linux or Windows, I suppose; and if you do that, please commit the .v files back to this branch. But it would be nice to have a longer-term solution for MacOS.

@mansky1
Copy link
Collaborator

mansky1 commented Jul 25, 2024

Great! This looks like it won't be too bad to port -- only a few of the files will require new work on vst_on_iris.

For MacOS, my impression is that the developers decided they're never going to support C11 threads. We could use #ifdef to fall back on Pthreads when C11 threads aren't available. I don't have a Mac machine to test on at the moment, but if you have time you can try out the attached and see if it works. That said, Pthreads and C11 threads disagree on the return type of spawned functions, so this might be impossible to smooth over.
threads.c.txt

@andrew-appel
Copy link
Collaborator Author

before you port to the other branch, let me get the CI working on this branch.

@andrew-appel andrew-appel mentioned this pull request Jul 26, 2024
Closed
@andrew-appel andrew-appel merged commit 6c978e6 into master Jul 28, 2024
23 checks passed
@andrew-appel andrew-appel deleted the compcert3.15 branch July 28, 2024 18:33
@andrew-appel andrew-appel mentioned this pull request Sep 19, 2024
Merged
proux01 added a commit to proux01/coq that referenced this pull request Sep 20, 2024
@proux01
Revert "[CI] Make VST compile its own compcert"
bf48731 
This reverts commit b767680
now that PrincetonUniversity/VST#781
has been merged, making VST compile again with CompCert master.
@proux01 proux01 mentioned this pull request Sep 20, 2024
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@mansky1 mansky1 Awaiting requested review from mansky1

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@andrew-appel @mansky1